inv-rel(A;B;f;finv) == (a:A, b:B. finv(b) = inl(a)  b = f(a)) & (a:A. finv(f(a)) = inl(a)) 

latex

---

clarification:

inv-rel(A;B;f;finv)
== (a:A, b:B. finv(b) = inl(a)  A+Unit  b = f(a)  B)
== & (a:A. finv(f(a)) = inl(a)  A+Unit) 

latex

Definitions	Unit, x:A. B(x), P  Q, P & Q, inv-rel(A;B;f;finv)
FDL editor aliases	inv-rel